(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)
(declare-fun v5 () Real)
(declare-fun v6 () Real)
(declare-fun v7 () Real)
(assert (let ((e8 1))
(let ((e9 7))
(let ((e10 (+ v5 v2)))
(let ((e11 (- v3 v0)))
(let ((e12 (+ e11 v6)))
(let ((e13 (* e11 e8)))
(let ((e14 (+ v6 v0)))
(let ((e15 (+ e14 e14)))
(let ((e16 (* e14 (- e9))))
(let ((e17 (- v4 v3)))
(let ((e18 (- e12)))
(let ((e19 (- e14 e16)))
(let ((e20 (+ v2 v2)))
(let ((e21 (* e17 e12)))
(let ((e22 (- e19)))
(let ((e23 (* (- e8) e14)))
(let ((e24 (- e15 e13)))
(let ((e25 (* e23 e21)))
(let ((e26 (* e14 e16)))
(let ((e27 (* e9 e15)))
(let ((e28 (+ v2 e25)))
(let ((e29 (+ e27 e17)))
(let ((e30 (* v6 e8)))
(let ((e31 (/ e9 (- e9))))
(let ((e32 (/ e8 e8)))
(let ((e33 (* e10 e9)))
(let ((e34 (+ v7 e18)))
(let ((e35 (* (- e8) e12)))
(let ((e36 (+ e13 e20)))
(let ((e37 (- e36)))
(let ((e38 (- e28 e10)))
(let ((e39 (- e18)))
(let ((e40 (- v1 e18)))
(let ((e41 (< e11 v3)))
(let ((e42 (= e36 v5)))
(let ((e43 (< e16 e37)))
(let ((e44 (= e21 e15)))
(let ((e45 (> e19 e39)))
(let ((e46 (distinct e14 e29)))
(let ((e47 (> e34 e30)))
(let ((e48 (distinct e37 e10)))
(let ((e49 (= e20 e28)))
(let ((e50 (<= e29 v0)))
(let ((e51 (<= e17 v0)))
(let ((e52 (>= e19 e16)))
(let ((e53 (>= e11 v3)))
(let ((e54 (= e16 e30)))
(let ((e55 (>= e36 e27)))
(let ((e56 (<= v4 e15)))
(let ((e57 (distinct e34 v0)))
(let ((e58 (< e26 v2)))
(let ((e59 (distinct e22 e17)))
(let ((e60 (<= e23 v2)))
(let ((e61 (distinct v6 e19)))
(let ((e62 (<= e35 e35)))
(let ((e63 (< e11 v1)))
(let ((e64 (>= e10 e39)))
(let ((e65 (distinct e35 e18)))
(let ((e66 (<= e10 e11)))
(let ((e67 (> e10 e39)))
(let ((e68 (<= e23 e29)))
(let ((e69 (= e23 e25)))
(let ((e70 (distinct e14 e14)))
(let ((e71 (<= e25 e12)))
(let ((e72 (distinct e25 e24)))
(let ((e73 (= e19 e16)))
(let ((e74 (distinct e35 e32)))
(let ((e75 (>= e30 e37)))
(let ((e76 (<= e27 e32)))
(let ((e77 (<= e24 e39)))
(let ((e78 (< e28 v4)))
(let ((e79 (= e17 e23)))
(let ((e80 (> v3 e26)))
(let ((e81 (>= e21 e19)))
(let ((e82 (<= e29 e14)))
(let ((e83 (= e17 v3)))
(let ((e84 (> v7 e21)))
(let ((e85 (>= e10 e37)))
(let ((e86 (= e34 e17)))
(let ((e87 (> e31 e28)))
(let ((e88 (<= v3 v4)))
(let ((e89 (>= v0 e33)))
(let ((e90 (< e19 v4)))
(let ((e91 (<= e38 e34)))
(let ((e92 (>= e12 e38)))
(let ((e93 (distinct v1 e18)))
(let ((e94 (>= e28 e20)))
(let ((e95 (= v0 e29)))
(let ((e96 (<= e10 e40)))
(let ((e97 (>= e40 e13)))
(let ((e98 (< e30 e31)))
(let ((e99 (> e28 v5)))
(let ((e100 (distinct v7 e30)))
(let ((e101 (> e37 e20)))
(let ((e102 (<= e13 v7)))
(let ((e103 (= e16 e27)))
(let ((e104 (distinct e38 e18)))
(let ((e105 (= e36 e20)))
(let ((e106 (> v0 e32)))
(let ((e107 (= e37 e38)))
(let ((e108 (>= e15 e25)))
(let ((e109 (distinct e21 e13)))
(let ((e110 (distinct v1 v4)))
(let ((e111 (> e27 e34)))
(let ((e112 (<= v6 e27)))
(let ((e113 (distinct e30 e29)))
(let ((e114 (<= e13 e33)))
(let ((e115 (< e11 e16)))
(let ((e116 (distinct e23 e40)))
(let ((e117 (distinct e34 e21)))
(let ((e118 (> e26 e25)))
(let ((e119 (> v1 e11)))
(let ((e120 (> e32 e14)))
(let ((e121 (distinct e27 e40)))
(let ((e122 (<= v0 e19)))
(let ((e123 (= e23 e38)))
(let ((e124 (<= v1 v2)))
(let ((e125 (= e39 v1)))
(let ((e126 (distinct v3 e40)))
(let ((e127 (>= e34 e26)))
(let ((e128 (<= e20 e11)))
(let ((e129 (> e23 e39)))
(let ((e130 (< e37 e26)))
(let ((e131 (< v4 v5)))
(let ((e132 (> e29 e20)))
(let ((e133 (< e38 v1)))
(let ((e134 (distinct v5 e22)))
(let ((e135 (<= e35 e30)))
(let ((e136 (>= e33 e28)))
(let ((e137 (< e14 e17)))
(let ((e138 (distinct e13 e28)))
(let ((e139 (<= e11 e16)))
(let ((e140 (<= v1 v5)))
(let ((e141 (> e19 v0)))
(let ((e142 (< e33 v0)))
(let ((e143 (< e29 e16)))
(let ((e144 (< e10 e10)))
(let ((e145 (> e34 e29)))
(let ((e146 (> e35 e30)))
(let ((e147 (<= v2 v2)))
(let ((e148 (< v3 e23)))
(let ((e149 (< e40 e37)))
(let ((e150 (<= e40 v1)))
(let ((e151 (<= e22 e22)))
(let ((e152 (> v7 v3)))
(let ((e153 (> e36 e35)))
(let ((e154 (>= e28 e24)))
(let ((e155 (distinct e30 v4)))
(let ((e156 (<= e16 e25)))
(let ((e157 (= e18 v1)))
(let ((e158 (= e12 e38)))
(let ((e159 (ite e83 e82 e69)))
(let ((e160 (ite e138 e129 e156)))
(let ((e161 (or e142 e101)))
(let ((e162 (= e105 e154)))
(let ((e163 (=> e64 e75)))
(let ((e164 (ite e99 e149 e114)))
(let ((e165 (xor e132 e57)))
(let ((e166 (and e134 e155)))
(let ((e167 (=> e135 e122)))
(let ((e168 (or e167 e93)))
(let ((e169 (not e74)))
(let ((e170 (xor e88 e157)))
(let ((e171 (xor e164 e46)))
(let ((e172 (and e115 e143)))
(let ((e173 (or e49 e120)))
(let ((e174 (= e133 e97)))
(let ((e175 (= e139 e94)))
(let ((e176 (and e53 e104)))
(let ((e177 (xor e124 e109)))
(let ((e178 (xor e70 e90)))
(let ((e179 (not e152)))
(let ((e180 (= e176 e119)))
(let ((e181 (or e48 e127)))
(let ((e182 (and e92 e44)))
(let ((e183 (not e58)))
(let ((e184 (=> e95 e78)))
(let ((e185 (ite e184 e63 e73)))
(let ((e186 (ite e86 e65 e62)))
(let ((e187 (and e144 e148)))
(let ((e188 (=> e183 e186)))
(let ((e189 (and e60 e117)))
(let ((e190 (xor e123 e91)))
(let ((e191 (not e131)))
(let ((e192 (xor e125 e174)))
(let ((e193 (ite e50 e188 e136)))
(let ((e194 (= e66 e153)))
(let ((e195 (and e161 e193)))
(let ((e196 (not e67)))
(let ((e197 (xor e162 e72)))
(let ((e198 (= e195 e197)))
(let ((e199 (not e52)))
(let ((e200 (ite e147 e180 e165)))
(let ((e201 (= e71 e168)))
(let ((e202 (and e199 e198)))
(let ((e203 (xor e178 e194)))
(let ((e204 (= e108 e160)))
(let ((e205 (xor e185 e59)))
(let ((e206 (and e106 e202)))
(let ((e207 (=> e51 e151)))
(let ((e208 (=> e81 e102)))
(let ((e209 (=> e107 e179)))
(let ((e210 (ite e121 e110 e146)))
(let ((e211 (ite e207 e169 e111)))
(let ((e212 (not e56)))
(let ((e213 (ite e61 e55 e55)))
(let ((e214 (xor e177 e190)))
(let ((e215 (ite e173 e213 e201)))
(let ((e216 (=> e191 e137)))
(let ((e217 (= e89 e170)))
(let ((e218 (ite e217 e112 e77)))
(let ((e219 (and e54 e84)))
(let ((e220 (xor e204 e47)))
(let ((e221 (xor e68 e181)))
(let ((e222 (=> e189 e189)))
(let ((e223 (ite e130 e210 e211)))
(let ((e224 (not e218)))
(let ((e225 (xor e128 e182)))
(let ((e226 (xor e118 e158)))
(let ((e227 (xor e209 e219)))
(let ((e228 (or e79 e41)))
(let ((e229 (ite e228 e175 e228)))
(let ((e230 (and e42 e159)))
(let ((e231 (not e126)))
(let ((e232 (xor e141 e172)))
(let ((e233 (ite e171 e222 e230)))
(let ((e234 (xor e208 e231)))
(let ((e235 (not e215)))
(let ((e236 (ite e227 e100 e203)))
(let ((e237 (and e187 e206)))
(let ((e238 (ite e163 e113 e223)))
(let ((e239 (= e229 e229)))
(let ((e240 (=> e192 e221)))
(let ((e241 (= e103 e216)))
(let ((e242 (and e96 e140)))
(let ((e243 (xor e224 e220)))
(let ((e244 (ite e200 e233 e85)))
(let ((e245 (and e244 e196)))
(let ((e246 (= e214 e225)))
(let ((e247 (=> e239 e98)))
(let ((e248 (= e243 e87)))
(let ((e249 (= e247 e245)))
(let ((e250 (ite e166 e240 e237)))
(let ((e251 (and e238 e226)))
(let ((e252 (ite e150 e45 e236)))
(let ((e253 (ite e43 e234 e43)))
(let ((e254 (ite e76 e212 e116)))
(let ((e255 (not e251)))
(let ((e256 (=> e242 e242)))
(let ((e257 (ite e252 e253 e232)))
(let ((e258 (= e248 e256)))
(let ((e259 (ite e250 e205 e249)))
(let ((e260 (= e246 e254)))
(let ((e261 (=> e255 e257)))
(let ((e262 (ite e258 e261 e235)))
(let ((e263 (or e80 e80)))
(let ((e264 (and e259 e260)))
(let ((e265 (not e241)))
(let ((e266 (not e262)))
(let ((e267 (xor e265 e264)))
(let ((e268 (= e266 e263)))
(let ((e269 (and e267 e145)))
(let ((e270 (or e268 e268)))
(let ((e271 (not e270)))
(let ((e272 (not e271)))
(let ((e273 (not e269)))
(let ((e274 (and e272 e273)))
e274
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
